Nuprl Lemma : q_le_wf
11,40
postcript
pdf
r
,
s
:rationals. q_le(
r
;
s
)
latex
Definitions
q_le(
r
;
s
)
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
rationals
wf
,
qeq
wf2
,
qsub
wf
,
qpositive
wf
,
bor
wf
origin
r,s:rationals. q_le(r; s) 
r,s:rationals. q_le(r; s) Tx:A. B(x)